/FONT#0=BASL30/FONT#1=BASI30/FONT#2=BASB30/FONT#3=NGR40
␈↓␈↓↓␈↓α␈↓β␈↓β
␈↓ ↓H
␈↓ β≥THE FORMAL EXPRESSION OF HUMAN REASONING
␈↓ ↓H

␈↓ ↓H

␈↓ ↓H
␈↓␈↓ α_The␈α⊗Mathematical␈α⊗Theory␈α⊗of␈α⊗Computation␈α⊗Group␈α⊗and␈α⊗the␈α⊗Representation␈α⊗Group␈α∃are
␈↓ ↓H
␈↓ ↓Hcurrently␈αunited␈αin␈αdeveloping␈αways␈αof␈αexpressing␈αhuman␈αreasoning␈αabout␈αmathematical␈αproofs,␈αthe
␈↓ ↓H
␈↓ ↓Hcorrectness␈α∪of␈α∪programs,␈α∪and␈α∪the␈α∪appropriateness␈α∪of␈α∪a␈α∪strategy␈α∪for␈α∪achieving␈α∪a␈α∩goal␈α∩in␈α∩terms
␈↓ ↓H
␈↓ ↓Hacceptable␈αto␈αa␈αproof-checker␈αcalled␈αFOL.␈αThe␈αwork␈αinvolves␈αdeveloping␈αFOL␈αso␈αthat␈αit␈αwill␈αaccept
␈↓ ↓H
␈↓ ↓Hreasoning␈αin␈αa␈αform␈αthat␈αseems␈α
closer␈α
to␈α
that␈α
we␈α
might␈α
be␈α
able␈α
to␈α
generate␈α
as␈α
well␈α
as␈α
have␈α
the␈α
ability
␈↓ ↓H
␈↓ ↓Hto␈α∞express␈α∞large␈α∞proofs␈α∞of␈α∞important␈α∞results␈α∞in␈α∞FOL.␈α∞For␈α∞the␈α∞moment␈α∞we␈α
shall␈α
put␈α
off␈α
explaining
␈↓ ↓H
␈↓ ↓Hwhy␈αthis␈αis␈αan␈αappropriate␈α
way␈α
of␈α
attacking␈α
the␈α
AI␈α
problem␈α
and␈α
will␈α
concentrate␈α
on␈α
explaining␈α
what
␈↓ ↓H
␈↓ ↓Hwe␈αare␈αdoing,␈αwhat␈αwe␈αhave␈αaccomplished␈αso␈αfar,␈αand␈αwhat␈αwe␈αexpect␈αto␈αaccomplish␈αin␈αthe␈αnext␈α
two
␈↓ ↓H
␈↓ ↓Hyears.
␈↓ ↓H

␈↓ ↓H
␈↓ α_FOL␈α∩is␈α∩a␈α∩proof-checker␈α∩for␈α∩first␈α⊃order␈α⊃logic␈α⊃supplemented␈α⊃by␈α⊃features␈α⊃intended␈α⊃to␈α⊃make
␈↓ ↓H
␈↓ ↓Hhuman␈αreasoning␈αtranslatable␈αstatement-by-statement␈αinto␈αreasoning␈αacceptable␈αto␈αthe␈αproof-checker.
␈↓ ↓H
␈↓ ↓HTo␈αavoid␈αmisunderstanding,␈αwe␈αshould␈αsay␈αthat␈αalmost␈αall␈αthe␈αproofs␈αthat␈αinterest␈αus␈αuse␈αset␈αtheory
␈↓ ↓H
␈↓ ↓Hwithin␈αthe␈αlogic␈αso␈αthat␈αfunctions␈αand␈αpredicates␈αcan␈αeffectively␈αbe␈αobjects␈αwhen␈αthis␈αis␈αwanted␈αas␈αit
␈↓ ↓H
␈↓ ↓Hoften␈α
is.
␈↓ ↓H

␈↓ ↓H
␈↓ α_FOL␈αis␈αbased␈αon␈αthe␈α"natural␈αdeduction"␈αstyle␈αof␈αrepresenting␈αthe␈αderivations␈αof␈αthe␈αtheorems
␈↓ ↓H
␈↓ ↓Hof␈α⊗first␈α⊗order␈α∃logic.␈α∃The␈α∃existing␈α∃supplements,␈α∃over␈α∃and␈α∃above␈α∃Prawitz's␈α∃description␈α∃of␈α∃the
␈↓ ↓H
␈↓ ↓Hunderlying␈α
formal␈α
system,␈α
include␈α
the␈α
following:
␈↓ ↓H

␈↓ ↓H
␈↓ α_1.␈α∃A␈α∃decision␈α∀procedure␈α∀for␈α∀tautological␈α∀reasoning␈α∀that␈α∀allows␈α∀any␈α∀purely␈α∀propositional
␈↓ ↓H
␈↓ ↓Hreasoning␈α⊂to␈α⊂be␈α⊂carried␈α⊂out␈α⊂in␈α⊂one␈α⊂step.␈α∂This␈α∂procedure␈α∂has␈α∂proved␈α∂entirely␈α∂practical␈α∂giving␈α∂an
␈↓ ↓H
␈↓ ↓Hanswer␈α
in␈α
a␈α
short␈α
time␈α
even␈α
when␈α
there␈α
are␈α
tens␈α
of␈α
premisses␈α
and␈α
tens␈α
of␈α
variables.
␈↓ ↓H

␈↓ ↓H
␈↓ α_2.␈α⊂A␈α⊂partial␈α⊂proof␈α⊂procedure␈α⊂for␈α⊂reasoning␈α⊂with␈α⊂equality.␈α⊂It␈α⊂has␈α∂proved␈α∂quite␈α∂useful␈α∂even
␈↓ ↓H
␈↓ ↓Hthough␈α
its␈α
capabilities␈α
are␈α
limited.
␈↓ ↓H

␈↓ ↓H
␈↓ α_3.␈α
The␈αintroduction␈αof␈αsort␈αrestrictions␈αon␈αthe␈αrange␈αof␈αvariables.␈αThis,␈αfor␈αexample,␈αallows␈αa
␈↓ ↓H
␈↓ ↓Huser␈α
to␈α
say␈α
"for␈α
all␈α
pawns␈α
...",␈α
rather␈α
than␈α
"for␈α
all␈α
X,␈α
if␈α
X␈α
is␈α
a␈α
pawn␈α
then␈α
...".
␈↓ ↓H

␈↓ ↓H
␈↓ α_4.␈αThe␈αability␈αto␈αattach␈αa␈αLISP␈αfunction␈αto␈αa␈αfunction␈αor␈αpredicate␈αsymbol␈αin␈αthe␈αlogic␈αand␈αto
␈↓ ↓H
␈↓ ↓Hgenerate␈α∩sentences␈α∩by␈α∩evaluating␈α⊃expressions.␈α⊃The␈α⊃importance␈α⊃of␈α⊃this␈α⊃comes␈α⊃from␈α⊃the␈α⊃fact␈α⊃that
␈↓ ↓H
␈↓ ↓Hhuman␈α⊃reasoning␈α⊃is␈α⊃not␈α⊃purely␈α⊃logical␈α⊃but␈α⊃involves␈α⊃observation␈α⊃and␈α⊃computations␈α⊃that␈α⊃are␈α⊂not
␈↓ ↓H
␈↓ ↓Hsuccinctly␈α
expressable␈α
as␈α
the␈α
application␈α
of␈α
rules␈α
of␈α
inference.
␈↓ ↓H

␈↓ ↓H
␈↓ α_4.␈α∂A␈α∂start␈α∂has␈α∂been␈α∞made␈α∞on␈α∞formalizing␈α∞metamathematics␈α∞of␈α∞FOL␈α∞based␈α∞languages␈α∞within
␈↓ ↓H
␈↓ ↓HFOL.
␈↓ ↓H

␈↓ ↓H
␈↓ α_5.␈α∩A␈α∩powerful␈α∩rule␈α∩for␈α∩manipulating␈α∩quantifiers␈α∩has␈α⊃been␈α⊃implemented␈α⊃that␈α⊃does␈α⊃certain
␈↓ ↓H
␈↓ ↓Hcomplex␈αchains␈αof␈αreasoning␈αin␈αa␈αsingle␈αstep.␈αThis␈αrule␈αis␈αessential␈αfor␈αthe␈αproposed␈αintroduction␈αof
␈↓ ↓H
␈↓ ↓Hsubgoaling␈α
facilities␈α
similiar␈α
to␈α
those␈α
in␈α
LCF.
␈↓ ↓H

␈↓ ↓H
␈↓ α_Much␈α∞of␈α∞our␈α∞previous␈α∞work␈α∞on␈α∞formalizing␈α∞proofs␈α∞of␈α∞the␈α∞correctness␈α
of␈α
computer␈α
programs
␈↓ ↓H
␈↓ ↓Hhas␈αbeen␈αbased␈αon␈αa␈αproof-checker␈αcalled␈αLCF␈α
for␈α
a␈α
logic␈α
of␈α
Robin␈α
Milner␈α
based␈α
on␈α
a␈α
logic␈α
of␈α
Dana
␈↓ ↓H
␈↓ ↓HScott.␈α⊃Within␈α⊃this␈α⊂formalism␈α⊂a␈α⊂number␈α⊂of␈α⊂programs␈α⊂were␈α⊂proved␈α⊂correct␈α⊂including␈α⊂some␈α⊂simple
␈↓ ↓H
␈↓ ↓Hcompilers␈α
and␈α
an␈α
interpreter␈α
for␈α
LISP.␈α
In␈α
the␈α
course␈αof␈αthis␈αwork,␈αsome␈αlimitations␈αof␈αLCF␈αturned
␈↓ ↓H
␈↓ ↓Hup,␈αbut␈αLCF␈αhas␈αmany␈αfeatures␈αfor␈αmaking␈αproofs␈αeasier␈αthat␈αhave␈αyet␈αto␈αbe␈αincorporated␈αin␈αFOL,
␈↓ ↓H
␈↓ ↓Hbecause␈α⊂FOL␈α⊂is␈α⊂a␈α⊂more␈α⊂complicated␈α∂logical␈α∂environment.␈α∂Our␈α∂preliminary␈α∂experience␈α∂with␈α∂FOL
␈↓ ↓H
␈↓ ↓Hshowed␈αthat␈αit␈αhad␈αto␈αbe␈αsubstantially␈αrewritten.␈αThis␈αtook␈αa␈αlot␈αof␈αtime,␈αbut␈αthe␈αnew␈αversion␈αis␈αnow
␈↓ ↓H
␈↓ ↓Hin␈α
a␈α
usable␈α
state.
␈↓ ↓H

␈↓ ↓H
␈↓ α_The␈α∩first␈α∩substantial␈α∩tasks␈α∩that␈α∩have␈α∩been␈α∩undertaken␈α∩with␈α⊃FOL␈α⊃are␈α⊃the␈α⊃verification␈α⊃of
␈↓ ↓H
␈↓ ↓Htheorems␈α∂in␈α∂elementary␈α∂number␈α∂theory.␈α∂Even␈α∂this␈α∂illustrates␈α∂that␈α∂much␈α∂of␈α∞ordinary␈α∞mathematical
␈↓ ↓H
␈↓ ↓Hreasoning␈α∪is␈α∪metamathematical␈α∪and␈α∪that␈α∪the␈α∩axiomatic␈α∩formalisms␈α∩ordinarily␈α∩proposed␈α∩are␈α∩not
␈↓ ↓H
␈↓ ↓Hadequate␈α∞to␈α∞express␈α∞the␈α∞proofs␈α∞that␈α∞are␈α∞actually␈α∞made.␈α
In␈α
fact␈α
the␈α
usual␈α
axiomatic␈α
formalisms␈α
are
␈↓ ↓H
␈↓ ↓Hadequate␈α∞only␈α∞in␈α
the␈α
sense␈α
that␈α
it␈α
is␈α
possible␈α
to␈α
prove␈α
informally␈α
that␈α
formal␈α
proofs␈α
exist,␈α
but␈α
the
␈↓ ↓H
␈↓ ↓Hformal␈αproofs␈αto␈αnot␈αexpress␈αthe␈αinformal␈αreasoning.␈αWe␈αare␈α
gradually␈α
correcting␈α
this␈α
by␈α
making␈α
the
␈↓ ↓H
␈↓ ↓Hproofs␈αand␈αmodifying␈αboth␈αFOL␈αand␈αour␈αaxiom␈αsystems␈αso␈αthat␈α
they␈α
informal␈α
reasoning␈α
can␈α
be␈α
well
␈↓ ↓H
␈↓ ↓Hexpressed.␈αThe␈αability␈αto␈αcarry␈αout␈αmetamathematical␈αreasoning␈αwithin␈αFOL,␈αand␈αhow␈αto␈αdo␈αthis␈αis
␈↓ ↓H
␈↓ ↓Hone␈α
of␈α
will␈α
be␈α
an␈α
active␈α
topic␈α
of␈α
research.
␈↓ ↓H

␈↓ ↓H
␈↓ α_The␈α
mathematical␈α
tools␈α
for␈α
expressing␈α
the␈α
Scott␈α
formalism␈α
on␈α
which␈α
LCF␈α
is␈α
based␈α
in␈α
FOL␈α
are
␈↓ ↓H
␈↓ ↓Hbeing␈α
developed,␈α
but␈α
the␈α
formalism␈α
has␈α
not␈α
yet␈α
reached␈α
the␈α
point␈α
where␈α
proofs␈α
are␈α
being␈α
written.
␈↓ ↓H

␈↓ ↓H
␈↓ α_Our␈αfirst␈αmajor␈αattempt␈αto␈αexpress␈αnon-mathematical␈αreaoning␈αhas␈αbeen␈αto␈αprove␈αthat␈αcertain
␈↓ ↓H
␈↓ ↓Hchess␈αproblems␈αhave␈αthe␈αstated␈αsolutions.␈αIf␈αthe␈αreasoning␈αhad␈αinvolved␈αmerely␈αfollowing␈αout␈αa␈αpart
␈↓ ↓H
␈↓ ↓Hof␈α∂the␈α∞move␈α∞tree␈α∞as␈α∞is␈α∞adequate␈α∞for␈α∞many␈α∞chess␈α∞problems,␈α∞the␈α∞formalization␈α∞problem␈α∞would␈α∞have
␈↓ ↓H
␈↓ ↓Hbeen␈αtrivial.␈αHowever,␈αin␈αthe␈αexamples␈αwe␈αhave␈αchosen,␈αa␈αsimple␈αtree␈αsearch␈αdoes␈αnot␈αcorrespond␈αto
␈↓ ↓H
␈↓ ↓Hthe␈αhuman␈αreasoning.␈αInstead␈αit␈αis␈αnecessary␈αto␈αargue␈αabout␈αwhat␈αone␈αplayer␈αis␈αdoing␈αwhile␈αanother
␈↓ ↓H
␈↓ ↓Hfollows␈α∞a␈α∞certain␈α∞path␈α∞in␈α∞general␈α∞terms,␈α∞because␈α∞tree␈α∞search␈α
would␈α
be␈α
too␈α
long␈α
and␈α
is␈α
unnecessary
␈↓ ↓H
␈↓ ↓Hbecause␈αthe␈αdifferent␈αpossible␈αmoves␈αhave␈αsimilar␈αeffects.␈αIn␈αthe␈αchess␈αreasoning,␈αit␈αhas␈αbeen␈αfound
␈↓ ↓H
␈↓ ↓Hthat␈αonly␈αa␈αpart␈α(albeit␈αan␈αimportant␈αpart)␈α
of␈α
the␈α
reasoning␈α
is␈α
appropriately␈α
carried␈α
out␈α
in␈α
logic.␈α
The
␈↓ ↓H
␈↓ ↓Hrest␈αis␈αbased␈αon␈αdirect␈αobservation␈αof␈αchess␈αboards␈αor␈αdirect␈αtree␈αsearch␈αand␈αis␈αappropriately␈αcarried
␈↓ ↓H
␈↓ ↓Hout␈α∞by␈α∞programs␈α∞attached␈α∞to␈α∞function␈α∞symbols␈α∞as␈α∞mentioned␈α∞above.␈α∞We␈α∞chose␈α∞this␈α∞group␈α
of␈α
chess
␈↓ ↓H
␈↓ ↓Hproblems,␈αbecause␈αeven␈αthough␈αthe␈αlaws␈αof␈αchess␈αare␈αcompletely␈αunderstood,␈α
the␈α
problems␈α
of␈α
parallel
␈↓ ↓H
␈↓ ↓Haction␈α⊃that␈α⊃arise␈α⊃both␈α⊃here␈α⊃and␈α⊃in␈α⊃real␈α⊃life␈α⊂situations␈α⊂are␈α⊂difficult␈α⊂to␈α⊂formalize.␈α⊂After␈α⊂we␈α⊂have
␈↓ ↓H
␈↓ ↓Hsuccessfully␈α∞formalized␈α∞the␈α∞chess␈α∞action,␈α∞we␈α∞will␈α∞be␈α∞ready␈α∞to␈α∞face␈α∞the␈α∞difficulties␈α∞of␈α
the␈α
real␈α
world
␈↓ ↓H
␈↓ ↓Hproblems.
␈↓ ↓H

␈↓ ↓H
␈↓ α_In␈α∂the␈α∂next␈α∂two␈α∂years,␈α∂it␈α∂looks␈α∂like␈α∞we␈α∞can␈α∞be␈α∞much␈α∞more␈α∞ambitious␈α∞in␈α∞terms␈α∞of␈α∞externally
␈↓ ↓H
␈↓ ↓Hvisible␈αaccomplishment␈αthan␈αwe␈α
have␈α
been␈α
in␈α
the␈α
last␈α
few␈α
years,␈α
because␈α
we␈α
are␈α
finally␈α
getting␈α
out␈α
of
␈↓ ↓H
␈↓ ↓Hthe␈α∞grubby␈α∞system␈α∞building␈α∞stage␈α∞and␈α∞will␈α
be␈α
able␈α
to␈α
put␈α
more␈α
resources␈α
into␈α
major␈α
extensions␈α
of
␈↓ ↓H
␈↓ ↓HFOL␈αand␈αespecially␈αinto␈αthe␈αuse␈αof␈αFOL␈αrather␈αthan␈αhaving␈αto␈αconcentrate␈α
on␈α
civilizing␈α
it.␈α
Here␈α
are
␈↓ ↓H
␈↓ ↓Hour␈α
goals:
␈↓ ↓H

␈↓ ↓H
␈↓ α_1.␈α∀Express␈α∀some␈α∪major␈α∪mathematical␈α∪proofs.␈α∪Examples␈α∪in␈α∪increasing␈α∪estimated␈α∪difficulty
␈↓ ↓H
␈↓ ↓Hinclude
␈↓ ↓H

␈↓ ↓H
␈↓ αha.␈α
The␈α
standard␈α
set-theoretic␈α
proof␈α
of␈α
Wilson's␈α
theorem.
␈↓ ↓H

␈↓ ↓H
␈↓ αhb.␈α∃Difficult␈α∃combinatorial␈α∃theorems␈α∃like␈α∃Ramsey's␈α∃theorem␈α∃or␈α∀van␈α∀der␈α∀Waerden's
␈↓ ↓H
␈↓ ↓Htheorem␈αon␈αarithmetic␈αprogressions␈αin␈αpartitions␈αof␈αthe␈αintegers␈αinto␈αsets.␈αWhen␈αwe␈αcan␈αdo␈αthese,␈αwe
␈↓ ↓H
␈↓ ↓Hwill␈α⊂have␈α⊂shown␈α⊂our␈α⊂ability␈α⊂to␈α⊂express␈α⊂mathematical␈α⊂reasoning␈α⊂of␈α⊂the␈α⊂complexity␈α∂that␈α∂occurs␈α∂in
␈↓ ↓H
␈↓ ↓Hresearch␈α
papers.
␈↓ ↓H

␈↓ ↓H
␈↓ αhc.␈α∩The␈α∩formalization␈α∩of␈α⊃the␈α⊃reasoning␈α⊃in␈α⊃Cohen's␈α⊃"Set␈α⊃Theory␈α⊃and␈α⊃the␈α⊃Continuum
␈↓ ↓H
␈↓ ↓HHypothesis".␈α⊃This␈α⊃reasoning␈α⊃is␈α⊃heavily␈α⊂metamathematical,␈α⊂and␈α⊂expressing␈α⊂it␈α⊂will␈α⊂require␈α⊂a␈α⊂good
␈↓ ↓H
␈↓ ↓Hformalization␈α
of␈α
metamathematics.
␈↓ ↓H

␈↓ ↓H
␈↓ α_We␈α∩target␈α∩these␈α∩tasks␈α∩at␈α∩three␈α∩months,␈α∩six␈α⊃months␈α⊃and␈α⊃eighteen␈α⊃months,␈α⊃and␈α⊃there␈α⊃is␈α⊃a
␈↓ ↓H
␈↓ ↓Hsubstantial␈α∞probability␈α∞that␈α∞we␈α∞will␈α∞be␈α∞diverted␈α∞from␈α∞the␈α∞last␈α∞by␈α
something␈α
else␈α
coming␈α
to␈α
appear
␈↓ ↓H
␈↓ ↓Hmore␈α∞appropriate.␈α∞By␈α∞the␈α∞end␈α∞of␈α∞the␈α∞next␈α∞contract␈α∞period,␈α∞we␈α∞expect␈α∞that␈α∞FOL␈α∞will␈α∞be␈α∞in␈α
a␈α
state
␈↓ ↓H
␈↓ ↓Hwhere␈αthe␈αreasoning␈αin␈αa␈α
mathematical␈α
paper␈α
can␈α
be␈α
expressed␈α
in␈α
a␈α
straightforward␈α
way␈α
by␈α
someone
␈↓ ↓H
␈↓ ↓Hwho␈α
understands␈α
the␈α
paper.
␈↓ ↓H

␈↓ ↓H
␈↓ α_2.␈α
Express␈α
a␈α
version␈α
of␈α
the␈α
Scott␈α
logic␈α
in␈αFOL␈αand␈αprove␈αsample␈αinterpreters,␈αcompilers␈αand
␈↓ ↓H
␈↓ ↓Happlication␈α∩programs␈α∩correct.␈α∩The␈α∩formalization␈α∩should␈α∩take␈α∩another␈α∩six␈α∩months␈α∩and␈α⊃then␈α⊃the
␈↓ ↓H
␈↓ ↓Happlications␈α
should␈α
begin␈α
to␈α
flow.
␈↓ ↓H

␈↓ ↓H
␈↓ α_3.␈αFinish␈αthe␈αchess␈αreasoning␈αproblems␈αnow␈αbeing␈αworked␈αon␈αand␈αget␈αa␈αgood␈αformalization␈αof
␈↓ ↓H
␈↓ ↓Hparallel␈α
action.␈α
It␈α
is␈α
difficult␈α
to␈α
say␈α
how␈α
long␈α
this␈α
last␈α
task␈α
will␈α
take.
␈↓ ↓H

␈↓ ↓H
␈↓ α_4.␈α
The␈α
following␈α
features␈α
are␈α
expected␈α
to␈α
be␈α
added␈α
to␈α
the␈α
FOL␈α
system.
␈↓ ↓H

␈↓ ↓H
␈↓ αha.␈α
goal␈α
structure␈α
similiar␈α
to␈α
the␈α
existing␈α
features␈α
in␈α
LCF.
␈↓ ↓H

␈↓ ↓H
␈↓ αhb.␈α
MFOL␈α
-␈α
i.e.␈α
the␈α
ability␈α
to␈α
do␈α
the␈α
metamathematical
␈↓ ↓H
␈↓ αhreasoning␈α
discussed␈α
above.␈α
This␈α
might␈α
include␈α
the␈α
ability
␈↓ ↓H
␈↓ αhof␈α
the␈α
user␈α
to␈α
prepare␈α
and␈α
call␈α
upon␈α
proof␈α
generating
␈↓ ↓H
␈↓ αhsubroutines␈α
so␈α
that␈α
FOL␈α
will␈α
gradually␈α
become␈α
a␈α
theorem
␈↓ ↓H
␈↓ αhprover␈α
as␈α
well␈α
as␈α
a␈α
proof-checker.
␈↓ ↓H

␈↓ ↓H
␈↓ αhc.␈α
an␈α
extensive␈α
definitional␈α
facility.␈α
This␈α
corresponds
␈↓ ↓H
␈↓ αhto␈α
the␈α
usual␈α
mathematical␈α
practice␈α
of␈α
defining␈α
new
␈↓ ↓H
␈↓ αhnotions␈α
and␈α
then␈α
operating␈α
with␈α
them␈α
in␈α
a␈α
valid␈α
way.
␈↓ ↓H

␈↓ ↓H
␈↓ αhd.␈α
a␈α
badly␈α
needed␈α
theorem␈α
making␈α
and␈α
using␈α
facility.␈α
At
␈↓ ↓H
␈↓ αhpresent␈α
there␈α
is␈α
no␈α
way␈α
to␈α
create␈α
a␈α
theorem,␈α
which␈α
could
␈↓ ↓H
␈↓ αhbe␈α
used␈α
later␈α
in␈α
another␈α
proof.
␈↓ ↓H

␈↓ ↓H
␈↓ ↓HThis␈α
will␈α
probably␈α
take␈α
six␈α
to␈α
nine␈α
months␈α
at␈α
the␈α
present␈α
rate␈α
of␈α
progress.
␈↓ ↓H


␈↓ α_Now␈αthat␈αwe␈αhave␈αexplained␈αwhat␈αwe␈αplan␈α
to␈α
do,␈α
it␈α
is␈α
worthwhile␈α
to␈α
say␈α
something␈α
about␈α
why
␈↓ ↓H
␈↓ ↓Hthe␈α∩approach␈α∩seems␈α∩appropriate␈α∩in␈α∩the␈α∩present␈α∩state␈α∩of␈α∩artificial␈α∩intelligence␈α∩research.␈α∩The␈α∩AI
␈↓ ↓H
␈↓ ↓Hproblem␈α∂has␈α∂always␈α∂been␈α∂regarded␈α∂as␈α∂difficult,␈α∂and␈α∂it␈α∂has␈α∂always␈α∂been␈α∞appropriate␈α∞to␈α∞find␈α∞good
␈↓ ↓H
␈↓ ↓Hsubproblems.␈α
Mostly␈α
this␈α
has␈α
been␈α
done␈αby␈αmaking␈αcomplete␈αsystems␈αlike␈αtheorem␈αprovers␈αor␈αchess
␈↓ ↓H
␈↓ ↓Hprograms␈αor␈αquestion␈αanswerers␈αand␈αrestricting␈αthe␈αdomain␈αof␈αoperation␈αof␈αthe␈αsystem␈αor␈α
settling␈α
for
␈↓ ↓H
␈↓ ↓Hlimited␈α
performance.␈α
This␈α
might␈α
be␈α
called␈α
a␈α
vertical␈α
subdivision␈α
of␈α
the␈α
AI␈α
problem.
␈↓ ↓H

␈↓ ↓H
␈↓ α_Vertical␈α⊂subdivision␈α⊂of␈α∂the␈α∂problem␈α∂is␈α∂appropriate,␈α∂but␈α∂so␈α∂is␈α∂horizontal␈α∂subdivision␈α∂which
␈↓ ↓H
␈↓ ↓Hconcentrates␈αon␈αan␈αaspect␈αof␈αintelligence.␈α
In␈α
the␈α
present␈α
case,␈α
we␈α
are␈α
relying␈α
on␈α
the␈α
division␈α
of␈α
the␈α
AI
␈↓ ↓H
␈↓ ↓Hproblem␈α
into␈α
the␈α
heuristic␈α
part␈α
and␈α
the␈α
epistemological␈α
part␈α
as␈α
proposed␈α
in␈α
(McCarthy␈αand␈αHayes
␈↓ ↓H
␈↓ ↓H1970),␈α↔and␈α↔the␈α↔present␈α↔work␈α⊗is␈α⊗on␈α⊗the␈α⊗epistemological␈α⊗part.␈α⊗Thus␈α⊗in␈α⊗mathematics,␈α⊗we␈α⊗are
␈↓ ↓H
␈↓ ↓Hconcentrating␈αon␈αbeing␈αable␈αto␈αexpress␈αformally␈αthe␈αreaoning␈αthat␈αis␈αactually␈αmade␈αin␈αthe␈αhope␈αthat
␈↓ ↓H
␈↓ ↓Hsuccess␈α
therein␈α
will␈α
provide␈α
a␈α
basis␈α
for␈α
programs␈α
that␈α
can␈α
generate␈α
real␈α
mathematical␈α
proofs.
␈↓ ↓H

␈↓ ↓H

␈↓ ↓H
PERSONNEL:
␈↓ ↓H

␈↓ ↓H
Staff:␈↓ α_ John McCarthy␈↓ ∧λ␈↓ ∧X␈↓ ¬(Student:  Arthur Thomas
␈↓ ↓H
 ␈↓ α_ Richard Weyhrauch␈↓ ∧X␈↓ ¬(␈↓ ¬x  Dave Poole
␈↓ ↓H
 ␈↓ α_ Bill Glassmire␈↓ ∧λ␈↓ ∧X␈↓ ¬(␈↓ ¬x  Dave Arnold
␈↓ ↓H
␈↓ α_ Bob Filman
␈↓ ↓H

␈↓ ↓H